COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	@make(report)
C00003 00003	This is a request to activate the second year of support for work begun
C00010 ENDMK
C⊗;
@make(report)
@begin(titlepage)
@begin(Titlebox)
@heading(Proposal to the
  National Science Foundation
  for continuation of
  Research into Mechanical Theorem Proving
  and
  the Development of EKL)
@end(titlebox)
@center(Computer Science Department
  Stanford University)
@blankspace(3 lines)
@center(John McCarthy)
@center(Professor of Computer Science)
@center(Principal Investigator)
@blankspace(3 lines)
@center(Jussi A. Ketonen)
@center(Research Associate)
@blankspace(3 lines)
@center(NSF Grant MCS 82-06565)
@blankspace(2 lines)
@center(@value(date))
@end(TitlePage)
This is a request to activate the second year of support for work begun
under Grant MCS82-06565, "Mechanical Theorem Proving and the Development of EKL."


@heading(Introduction)
	Ketonen has been working on further development of EKL,
an interactive proof checker in high order predicate calculus.

         The emphasis has been on creating a system and a language
which would allow the expression and verification of mathematical 
facts in a direct and natural way. The approach taken has been quite
successful: Ketonen has been able to produce an elegant and eminently
readable proof of Ramsey's theorem in under 100 lines. At the same time
EKL is versatile enough to be able to verify the associativity of the LISP
append function in just one line.

	The above results  are important in that they indicate that
programs previously thought to be too complex for 
mechanical verification are now within the reach of sufficiently powerful
proof checking systems.

@heading(Accomplishments)

A manual reflecting the state of EKL during December 1982 was written
by Ketonen and Joe Weening, a graduate assistant.

EKL has been tested by its use in CS206, a course on Lisp programming
at Stanford. As homework assignments,
students used it to prove facts about Lisp programs.

One of the outgrowths of this development work has been a 
formalization of the underlying logic of EKL.
EKL was based on a high order predicate logic since we felt that it
is important to be able to discuss functionals and lambda abstraction
in a natural way.
At the same time it seemed to us 
that the currently fashionable formalizations 
of high order logic were still inadequate for expressing
mathematical facts. Our approach was to gradually
modify the logic of EKL to accomodate intuitively straightforward
extensions without worrying too much about the formal underpinnings.
It is satisfying to note that we have now come a full circle:
Ketonen has shown that the logic of EKL can be formally expressed
(along with its consistency proofs, etc.) in a very elegant and precise
way -- in fact, in a more elegant way than the logics we started out with.
This theory also embodies the way EKL can talk about meta-theoretic
entities -- to our knowledge one of the first instances of a logical
theory of mathematics that can discuss denotations in a coherent way.
The meta-theoretic machinery of EKL has been implemented. 
Ketonen and Weening are in the process of writing a paper on this.

A large amount of effort has been spent on the EKL rewriting system --
currently the most powerful and versatile component of EKL.
Ketonen has come up with a new architecture for rewriting systems that
is quite different from the ones currently used, say, by Boyer and Moore.
Accompanying the rewriter there is also a notion of a language for
rewriting -- how to control the process through simple instructions to EKL.
This has turned out to be a fairly powerful tool in reducing the
lengths of proofs in EKL.

 Another direction for Ketonen's research is the use of high order unification
in rewriting: Ketonen has shown that the high order unification 
algorithm of Huet terminates when the unifiable variables come from
only one side, a situation that occurs naturally in rewriting.
As is well known, the termination problem for high order
unification is unsolvable in general.
This algorithm has now been implemented.  It seems to work quite nicely in practice.

The paper by Ketonen and Weyhrauch on a natural decidable 
fragment of predicate calculus has been submitted for publication.
Many interesting problems remain: for example, the proper use 
of equalities in the decision procedure given by this fragment and
its correct implementation. In implementing a new version of this
decision procedure Ketonen intends to use and refine the
notion of postponement developed by McCarthy.